package no.uio.ifi.cop.prover;

import java.util.LinkedList;
import java.util.Set;
import java.util.HashSet;

import no.uio.ifi.cop.common.Log;
import no.uio.ifi.cop.common.Global;
import no.uio.ifi.cop.util.Stoppable;
import no.uio.ifi.cop.util.Tuple;
import no.uio.ifi.cop.cl.Theory;
import no.uio.ifi.cop.cl.RHS;
import no.uio.ifi.cop.cl.Conjunction;
import no.uio.ifi.cop.cl.Constant;
import no.uio.ifi.cop.cl.Variable;
import no.uio.ifi.cop.cl.Term;
import no.uio.ifi.cop.cl.Substitution;
import no.uio.ifi.cop.cl.Predicate;
import no.uio.ifi.cop.cl.Axiom;
import no.uio.ifi.cop.parse.formula.Parser;
import no.uio.ifi.cop.parse.formula.TermFactory;

// FIXME
import no.uio.ifi.cop.prover.simple.SimpleRuleMatcher;

/**
 * This class is able to prove coherent theorems
 * as long as a sound RuleFinder is supplied.
 *
 *
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */

public class Prover implements Stoppable{

    private boolean valid;
    private boolean running;
    private boolean timeLeft;
    private boolean keepGraph;
    private boolean pathCount;
    private boolean singleMatch;
    private boolean ignore;

    private int maxPath;

    private Theory theory;
    private FactSet facts; // current set of facts
    private RuleFinder rulefinder; // current branch
    private LinkedList<Tuple<FactSet, RuleFinder>> paths;
    private LinkedList<Node> graph;
    private Node root;

    public Prover(){
        this(false);
    }

    public Prover(boolean keepGraph){
        this.keepGraph = keepGraph;
        TermFactory.reset();
        pathCount = Global.getBool("-paths");
        singleMatch = Global.getBool("-single");
        maxPath = Global.getInt("-maxpaths");
        ignore  = Global.getBool("-ignore");
    }

    public boolean isValid(){
        Log.info(" PATHS LEFT %s\n", paths.size());
        return valid;
    }

    public boolean graphStored(){
        return keepGraph;
    }

    private void init(){

        if( theory == null ){
            Log.fatal("theory == null: missing something to prove here");
        }

        if( rulefinder == null ){
            Log.fatal("rulefinder == null: missing RuleFinder");
        }

        paths = new LinkedList<Tuple<FactSet, RuleFinder>>();
        facts = new FactSet();
        graph = new LinkedList<Node>();

        for(Axiom ax : theory){
            switch( ax.getType() ){
                case Axiom.FACTRULE: 
                    addPlainFacts( ax );
                    break;
                default:
                    rulefinder.addRule( ax );
            }
        }

        paths.add( new Tuple<FactSet, RuleFinder>( facts, rulefinder ));

        if( keepGraph ){
            createRootNode();
        }

        Log.debug("%s", rulefinder);
    }

    // creates a dummy Axiom: true => all_facts
    // and adds 'true' and 'all_facts' as nodes in the graph.
    // it is only used for drawing the dotGraph...
    private void createRootNode(){
        
        Node.resetCounter();

        Node node, tmp;
        Conjunction lhs, conjunct;
        Axiom ax = new Axiom();
        Predicate pred = new Predicate("true");
        lhs = new Conjunction();
        RHS rhs = new RHS();

        lhs.add( pred );
        ax.setLHS( lhs );

        node = new Node( lhs );
        root = node;

        conjunct = new Conjunction();

        for( Predicate p : facts.iterUnshuffled() ){
            conjunct.add( p );
            rhs.add( p );
        }

        tmp = new Node( conjunct );

        ax.setRHS(rhs);

        root.addSubstitution( new Substitution() );
        root.addAxiom( ax );
        root.extend(tmp);

        graph.add( tmp );
    }


    public String getDotGraph(String header, int max){

        if( root == null ){
            Log.fatal(" root of graph == null!, can't draw graph");
        }

        StringBuilder sb = new StringBuilder();
        sb.append("digraph mygraph {\n");
        sb.append(header);
        sb.append("  rankdir=TB;\n");

        root.setMax( max );
        root.dotGraph(sb);

        sb.append("\n}\n");
        return sb.toString();
    }

    public String getDotGraph(String header){
        return getDotGraph( header, Integer.MAX_VALUE );
    }

    public void run(){

        Log.debug("Prover.run()");

        init();

        timeLeft = true;
        running  = true;
        valid    = false;

        Tuple<Axiom, Substitution> found;
        Tuple<FactSet, RuleFinder> tmp;
        Axiom ax;

        while( timeLeft && proceed() ){ 

            Log.debug("%s", facts);

            if( ! singleMatch ){
                // match all new facts against rules
                for( Predicate p : facts.iterUnmatched() ){
                    Log.debug(" matching '%s' against all rules", p);
                    rulefinder.addPredicate( p );
                }
                // unmatched -> matched
                facts.update();
            }else{
                Predicate pred = facts.getSingle();
                if( pred != null ){
                    rulefinder.addPredicate( pred );
                    facts.updateSingle( pred );
                }
            }

            // hopefully we were able to match a rule..
            found = rulefinder.getNextMatch();

            Log.debug("%s", rulefinder);
            Log.debug("found: %s", found);


            if( found != null ){

                ax = found.first();

                switch( ax.getType() ){
                    case Axiom.GOALRULE:
                        if( handleGoal( found ) ){
                            Log.debug(" handleGoal = ok");
                            timeLeft = false; // we are done
                            valid    = true;
                        }
                        break;
                    case Axiom.PLAINRULE:
                        handlePlain( found );
                        break;
                    case Axiom.DISJUNCTRULE:
                        handleDisjunct( found );
                        break;
                    case Axiom.EXISTRULE:
                        handleExistRule( found );
                        break;
                    case Axiom.EXISTDISRULE:
                        handleExistDisRule( found );
                        break;
                    default:
                        Log.fatal("This should never happen");

                }
            }

            // abort if path count is higher than maxPath
            if (maxPath > 0 && paths.size() > maxPath){
                timeLeft = false;
            }
        }

        running = false;
    }

    private boolean proceed(){

        Tuple<FactSet, RuleFinder> tuple;
        tuple = paths.peek();

        FactSet fs = tuple.first();
        RuleFinder rlf = tuple.second();

        if( fs.hasNewFacts()  ){
            Log.debug(" proceed - hasNewFacts ");
            return true;
        }

        if( ! rlf.exhausted() ){
            Log.debug(" proceed - ! exhausted ");
            return true;
        }

        Log.debug(" ! proceed");
        return false;
    }

    public boolean isRunning(){
        Log.debug(" Prover.isRunning() ");
        return running;
    }

    public void stop(){
        Log.debug(" Prover.stop()");
        timeLeft = false;
        if( rulefinder != null ){
            rulefinder.stop();
        }
    }

    @SuppressWarnings("unchecked")
        private void addPlainFacts(Axiom ax){
            Log.debug(" addPlainFacts() %s ",ax);
            for( Term t : ax.getRHS().iterFacts() ){
                facts.add( (Predicate) t );
            }
        }

    private boolean handleGoal(Tuple<Axiom, Substitution> tuple){

        Log.info("%s", facts);

        Log.info(" GOALRULE    : %s\n with        : %s",
                 tuple.first(), tuple.second());

        paths.poll(); // pop off closed path...

        if( keepGraph ){
            Node tmp = graph.poll();
            if( tmp == null ){
                Log.fatal(" graph.poll() == null ");
            }else{
                tmp.addAxiom( tuple.first() );
                tmp.addSubstitution( tuple.second() );
                Node res = new Node( tuple.first().getRHS().clone().get( 0 ) );
                tmp.extend( res );
            }
        }

        Log.info(" PATH COUNT : %d", paths.size() );

        if(pathCount){
            System.out.printf(" paths left: %d\r", paths.size());
        }

        if( paths.size() == 0 ){// it was the last path
            Log.debug(" handleGoal -> we are done ");
            return true;
        }else{// start with next path
            Log.debug(" handleGoal -> we are not done ");
            Tuple<FactSet, RuleFinder> next = paths.peek();
            facts      = next.first();
            rulefinder = next.second();
            Log.debug("%s", facts);
            return false;
        }
    }


    @SuppressWarnings("unchecked")  
        private void handlePlain(Tuple<Axiom, Substitution> tuple){

        // clone RHS apply substitution to result
        RHS rhsClone = tuple.first().getRHS().clone().apply( tuple.second() );

        Log.info("%s", facts);
        Log.info(" PLAINRULE   : %s\n with        : %s\n gives       : %s",
                tuple.first(), tuple.second(), rhsClone);
        for( Term t : rhsClone.iterFacts() ){
            Log.debug(" addNewFact: %s ", t);
            facts.add( (Predicate) t );
        }

        if( keepGraph ){
            Node tmp = graph.poll();
            tmp.addAxiom( tuple.first() );
            tmp.addSubstitution( tuple.second() );
            Node res = new Node( rhsClone.get(0) );
            tmp.extend( res );
            graph.addFirst( res );
        }
    }


    private void handleDisjunct(Tuple<Axiom, Substitution> tuple){

        // clone RHS apply substitution to result
        RHS rhsClone = tuple.first().getRHS().clone().apply( tuple.second() );

        Log.info("%s", facts);
        Log.info(" DISJUNCTRULE: %s\n with        : %s\n gives       : %s",
                tuple.first(), tuple.second(), rhsClone);

        if( keepGraph ){
            Node tmp = graph.peek();
            tmp.addAxiom( tuple.first() );
            tmp.addSubstitution( tuple.second() );
        }

        fork( rhsClone );
    }

    @SuppressWarnings("unchecked") private void 
        handleExistRule(Tuple<Axiom, Substitution> tuple){

        // clone RHS apply substitution to result
        RHS rhsClone = tuple.first().getRHS().clone().apply( tuple.second() );

        Conjunction conjunct;

        if( rhsClone.length() != 1 ){
            Log.fatal(" this should never happen");
        }

        conjunct = rhsClone.get(0);

        if( existMatch( conjunct ) ){
            Log.debug(" already here: %s", conjunct );
            return;
        }else{

            Substitution subst = getConjunctSubstitution( conjunct );
            conjunct.apply( subst );

            Log.info("%s", facts);
            Log.info(" EXISTRULE   : %s\n with        : %s\n gives       : %s",
                    tuple.first(), tuple.second().join( subst ), conjunct);

            for( Term t : conjunct ){
                facts.add( (Predicate) t);
            }

            if( keepGraph ){
                Node tmp = graph.poll();
                tmp.addAxiom( tuple.first() );
                tmp.addSubstitution( tuple.second() );
                Node res = new Node( conjunct );
                tmp.extend( res );
                graph.addFirst( res );
            }
        }
    }

    private void handleExistDisRule(Tuple<Axiom, Substitution> tuple){

        // clone RHS apply substitution to result
        RHS rhsClone = tuple.first().getRHS().clone().apply( tuple.second() );

        for( Conjunction c : rhsClone.iterConjunction() ){
            if( existMatch( c ) ){
                Log.debug(" already here: %s", c);
                return;
            }
        }

        // when we get here we have no matching conjunct in factset

        Substitution subst = getDisjunctSubstitution( rhsClone );
        rhsClone.apply( subst );

        Log.info("%s", facts);
        Log.info(" EXISTDISRULE: %s\n with        : %s\n gives       : %s",
                tuple.first(), tuple.second().join( subst ), rhsClone);

        if( keepGraph ){
            Node tmp = graph.peek();
            tmp.addAxiom( tuple.first() );
            tmp.addSubstitution( tuple.second() );
        }

        fork( rhsClone );
    }

    private boolean existMatch(Conjunction conjunct){

        Log.debug(" existMatch(%s)", conjunct);

        if(ignore){
            return false;
        }

        Axiom ax = new Axiom();
        ax.setLHS( conjunct );

        SimpleRuleMatcher rlmatcher = new SimpleRuleMatcher( -1, ax );

        for( Predicate p : facts.iterMatched() ){
            rlmatcher.match( p );
        }

        Substitution subst = rlmatcher.getNextMatch(false);
        return  subst != null;

    }

    @SuppressWarnings("unchecked")
    private void fork( RHS rhsClone ){

        RuleFinder tmpRLfinder;
        FactSet    tmpFactSet;
        Conjunction tmpConjuction;
        // just for printing/formatting purposes
        Node tmpChild, tmpParent;

        int max = rhsClone.length();
        // NOTE: i starts at 1, first conjunct adds facts to current path
        for(int i = 1; i < max; i++){
            tmpRLfinder   = rulefinder.clone();
            tmpFactSet    = facts.clone();
            tmpConjuction = rhsClone.get( i );
            Log.debug(" fork ");
            for( Term t : tmpConjuction ){
                Log.debug(" adding fact (newpath) %s", t);
                tmpFactSet.add( (Predicate) t );
            }
            Log.debug("--------\n%s\n%s\n--------", tmpFactSet, tmpRLfinder);
            paths.add(new Tuple<FactSet, RuleFinder>(tmpFactSet, tmpRLfinder));

            if( keepGraph ){
                tmpParent = graph.peek(); 
                tmpChild  = new Node( tmpConjuction );
                tmpParent.extend( tmpChild );
                graph.add( tmpChild );
            }
        }

        // add first conjunct to current path
        tmpConjuction = rhsClone.get( 0 );
        for( Term t : tmpConjuction ){
            facts.add( (Predicate) t );
        }

        if( keepGraph ){
            tmpParent = graph.poll();
            tmpChild  = new Node( tmpConjuction );
            tmpParent.extend( tmpChild );
            graph.addFirst( tmpChild );
        }

        Log.info(" PATH COUNT : %d", paths.size() );
        if( pathCount ){
            System.out.printf(" paths left: %d\r", paths.size());
        }
    }

    private Substitution getDisjunctSubstitution(RHS rhs){
        Set<String> variables = new HashSet<String>(); 
        rhs.gatherVariables( variables );
        return vars2subst( variables );
    }

    private Substitution getConjunctSubstitution(Conjunction conjunct){
        Set<String> variables = new HashSet<String>(); 
        conjunct.gatherVariables( variables );
        return vars2subst( variables );
    }

    private Substitution vars2subst( Set<String> set ){

        Substitution subst = new Substitution();
        Constant c_tmp;
        Variable v_tmp;

        for( String v : set ){
            v_tmp = new Variable( v );
            c_tmp = TermFactory.getFreshConstant(); 
            if(! subst.add(v_tmp, c_tmp) ){
                Log.fatal(" this should never happen");
            }
        }
        return subst;
    }

    public void addRuleFinder(RuleFinder rulefinder){
        this.rulefinder = rulefinder;
    }

    public void addTheory(Theory theory){
        this.theory = theory;
    }

    public void addTheoryFileName(String filename){

        Parser parser = Parser.getParser();

        long t0 = System.currentTimeMillis();
        Theory theory = parser.parseFile(filename);
        long t1 = System.currentTimeMillis();

        StringBuilder sb = new StringBuilder();
        sb.append("========================================================\n");
        sb.append(" Parsed file '%s' in: %d ms \n");
        sb.append("========================================================\n");
        sb.append("\n%s\n");
        Log.info(sb.toString(), filename, (t1 - t0), theory);

        addTheory(theory);
    }
}
